\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $a$:ecl(${\it ds}$;${\it da}$), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$;${\it da}$),\+
\\[0ex]$L$:event{-}info(${\it ds}$;${\it da}$) List.
\-\\[0ex](\=$\forall$$L$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]ecl{-}trans{-}normal($v$) \& ($\forall$$n$:$\mathbb{N}^{+}$. ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$v$)($n$,$L$) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($v$)))
\\[0ex]\& (\=$\forall$$n$:$\mathbb{N}$.\+
\\[0ex]($\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List. ${\it L'}$ $\leq$ $L$ \& ecl{-}halt(${\it ds}$;${\it da}$;$a$)($n$,${\it L'}$))
\\[0ex]$\Leftrightarrow$
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;$v$)($n$,$L$))
\-\\[0ex]\& ($\forall$$m$:$\mathbb{N}$. ecl{-}act(${\it ds}$;${\it da}$;$m$;$a$)($L$) $\Leftrightarrow$ ecl{-}trans{-}act(${\it ds}$;${\it da}$;$v$)($m$,$L$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$$n$:$\mathbb{N}$.\+
\\[0ex](\=$\exists$${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List.\+
\\[0ex]${\it L'}$ $\leq$ $L$
\\[0ex]\& 0$<$$n$
\\[0ex]\& star{-}append(event{-}info(${\it ds}$;${\it da}$);ecl{-}halt(${\it ds}$;${\it da}$;$a$)(0);ecl{-}halt(${\it ds}$;${\it da}$;$a$)($n$))(${\it L'}$))
\-\\[0ex]$\Leftrightarrow$
\\[0ex]ecl{-}trans{-}halt2(${\it ds}$;${\it da}$;reset{-}ecl{-}tuple($v$))($n$,$L$))
\-
\end{tabbing}